﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Epsilon.Expr;

namespace Epsilon
{
    public static class PidUtil
    {
        private static int pid = 0;
        private static int pide = 0;

        private static void Error(string e)
        {
            throw new PidLabelException(e);
        }

        public static PidVar NewVar()
        {
            pid++;
            return new PidVar("_P" + pid.ToString());
        }

        public static PidExpr NewPid()
        {
            pide++;
            return new PidExpr("_p" + pide.ToString(), -1, -1);
        }

        public static PidFun AlphaConvert(PidFun f, Dictionary<PidVar, PidVar> sub, bool join)
        {
            List<PidRLabel> args = new List<PidRLabel>();
            for (int i = 0; i < f.Args.Count; i++)
                args.Add(Alpha(sub, f.Args[i]));

            Dictionary<PidVar, PidBase> newSub = new Dictionary<PidVar, PidBase>();
            foreach (PidVar v in sub.Keys)
            {
                List<PidVar> l = new List<PidVar>();
                l.Add(sub[v]);
                newSub.Add(v, new PidBase(l, null)); 
            }

            PidLabel ret = Sub(newSub, f.Ret, join);
            return new PidFun(args, ret);
        }

        # region Join

        public static PidLabel Join(List<PidLabel> labels)
        {
            if (labels.Count == 0)
                return new PidBase(null, null);

            PidLabel p = labels[0];
            for (int i = 1; i < labels.Count; i++)
                p = Join(p, labels[i]);

            return p;
        }

        public static PidLabel Join(PidLabel left, PidLabel right)
        {
            if ((left is PidBase) && ((PidBase)left).IsEmpty)
                return right;
            else if ((right is PidBase) && ((PidBase)right).IsEmpty)
                return left;

            if ((left is PidBase) && (right is PidBase))
                return Join((PidBase)left, (PidBase)right);
            else if ((left is PidTuple) && (right is PidTuple))
                return Join((PidTuple)left, (PidTuple)right);
            else if ((left is PidFun) && (right is PidFun))
                return Join((PidFun)left, (PidFun)right);
            Error("Unable to compute the join of " + left.ToString() +
                " and " + right.ToString());
            return null;
        }

        public static PidBase Join(PidBase left, PidBase right)
        {
            List<PidExpr> pids = null;
            List<PidVar> pidvs = null;

            if (left.Pids != null)
            {
                pids = new List<PidExpr>();
                foreach (PidExpr e in left.Pids)
                    pids.Add(e);
            }
            if (left.Pidvs != null)
            {
                pidvs = new List<PidVar>();
                foreach (PidVar v in left.Pidvs)
                    pidvs.Add(v);
            }

            if (right.Pids != null)
            {
                if (pids == null)
                    pids = right.Pids;
                else
                    pids.AddRange(right.Pids);
            }
            if (right.Pidvs != null)
            {
                if (pidvs == null)
                    pidvs = right.Pidvs;
                else
                    pidvs.AddRange(right.Pidvs);
            }

            return new PidBase(
                (pidvs == null) ? null : new List<PidVar>(pidvs.Distinct()),
                (pids == null) ? null : new List<PidExpr>(pids.Distinct())
                );
        }

        public static PidTuple Join(PidTuple left, PidTuple right)
        {
            if (left.Labels.Count != right.Labels.Count)
                Error("Unable to join tuples of different lengths: "
                    + left.ToString() + " and " + right.ToString());

            List<PidLabel> labels = new List<PidLabel>();
            for (int i = 0; i < left.Labels.Count; i++)
                labels.Add(Join(left.Labels[i], right.Labels[i]));
            return new PidTuple(labels);
        }

        public static PidFun Join(PidFun left, PidFun right)
        {
            // check for alpha conversion
            List<PidRLabel> args = left.Args;
            PidLabel lBody = left.Ret;
            PidLabel rBody = right.Ret;

            if (left != right)
            {
                args = new List<PidRLabel>();
                foreach (PidRLabel a in left.Args)
                    args.Add(CreateNewAlpha(a));
                // Create a pid tuple for ease of calculating the substitution
                PidRTuple lsrc = new PidRTuple(left.Args);
                PidRTuple rsrc = new PidRTuple(right.Args);
                PidRTuple dest = new PidRTuple(args);
                Dictionary<PidVar, PidVar> lsub = Equate(lsrc, dest);
                Dictionary<PidVar, PidVar> rsub = Equate(rsrc, dest);
                lBody = AlphaConvert(left, lsub, true).Ret;
                rBody = AlphaConvert(right, rsub, true).Ret;
            }

            PidLabel ret = Join(lBody, rBody);
            return new PidFun(args, ret);
        }

        #endregion

        #region Meet

        public static PidLabel Meet(List<PidLabel> labels)
        {
            if (labels.Count == 0)
                return new PidBase(null, null);

            PidLabel p = labels[0];
            for (int i = 1; i < labels.Count; i++)
                p = Meet(p, labels[i]);

            return p;
        }

        public static PidLabel Meet(PidLabel left, PidLabel right)
        {
            if ((left is PidBase) && ((PidBase)left).IsEmpty)
                return right;
            else if ((right is PidBase) && ((PidBase)right).IsEmpty)
                return left;

            if ((left is PidBase) && (right is PidBase))
                return Meet((PidBase)left, (PidBase)right);
            else if ((left is PidTuple) && (right is PidTuple))
                return Meet((PidTuple)left, (PidTuple)right);
            else if ((left is PidFun) && (right is PidFun))
                return Meet((PidFun)left, (PidFun)right);
            Error("Unable to compute the meet of " + left.ToString() +
                " and " + right.ToString());
            return null;
        }

        public static PidBase Meet(PidBase left, PidBase right)
        {
            List<PidExpr> pids = null;
            List<PidVar> pidvs = null;

            if (left.Pids != null)
            {
                pids = new List<PidExpr>();
                foreach (PidExpr e in left.Pids)
                    pids.Add(e);
            }
            if (left.Pidvs != null)
            {
                pidvs = new List<PidVar>();
                foreach (PidVar v in left.Pidvs)
                    pidvs.Add(v);
            }

            if (right.Pids != null)
            {
                if (pids == null)
                    pids = right.Pids;
                else 
                    pids = new List<PidExpr>(pids.Intersect(right.Pids));
            }
            if (right.Pidvs != null)
            {
                if (pidvs == null)
                    pidvs = right.Pidvs;
                else
                    pidvs = new List<PidVar>(pidvs.Concat(right.Pidvs).Distinct());
            }

            return new PidBase(pidvs, pids);
        }

        public static PidTuple Meet(PidTuple left, PidTuple right)
        {
            if (left.Labels.Count != right.Labels.Count)
                Error("Unable to meet tuples of different lengths: "
                    + left.ToString() + " and " + right.ToString());

            List<PidLabel> labels = new List<PidLabel>();
            for (int i = 0; i < left.Labels.Count; i++)
                labels.Add(Meet(left.Labels[i], right.Labels[i]));
            return new PidTuple(labels);
        }

        public static PidFun Meet(PidFun left, PidFun right)
        {
            // check for alpha conversion
            PidRTuple largs = new PidRTuple(left.Args);
            PidRTuple rargs = new PidRTuple(right.Args);

            List<PidRLabel> args = left.Args;
            PidLabel lBody = left.Ret;
            PidLabel rBody = right.Ret;

            if (largs != rargs)
            {
                args = new List<PidRLabel>();
                foreach (PidRLabel a in left.Args)
                    args.Add(CreateNewAlpha(a));
                // Create a pid tuple for ease of calculating the substitution
                PidRTuple lsrc = new PidRTuple(left.Args);
                PidRTuple rsrc = new PidRTuple(right.Args);
                PidRTuple dest = new PidRTuple(args);
                Dictionary<PidVar, PidVar> lsub = Equate(lsrc, dest);
                Dictionary<PidVar, PidVar> rsub = Equate(rsrc, dest);
                lBody = AlphaConvert(left, lsub, false).Ret;
                rBody = AlphaConvert(right, rsub, false).Ret;
            }

            PidLabel ret = Meet(lBody, rBody);
            return new PidFun(args, ret);
        }

        #endregion

        #region Vars

        public static List<PidVar> Vars(PidLabel l)
        {
            if (l is PidBase)
                return Vars((PidBase)l);
            else if (l is PidTuple)
                return Vars((PidTuple)l);
            else if (l is PidFun)
                return Vars((PidFun)l);
            else
                Error("Invalid process label");
            return null;
        }

        public static List<PidVar> Vars(PidBase b)
        {
            return b.Pidvs;
        }

        public static List<PidVar> Vars(PidTuple t)
        {
            List<PidVar> v = new List<PidVar>();
            for (int i = 0; i < t.Labels.Count; i++)
                v.AddRange(Vars(t.Labels[i]));
            return new List<PidVar>(v.Distinct());
        }

        public static List<PidVar> Vars(PidFun f)
        {
            List<PidVar> v = new List<PidVar>();
            for (int i = 0; i < f.Args.Count; i++)
                v.AddRange(Vars(f.Args[i]));
            v.AddRange(Vars(f.Ret));
            return new List<PidVar>(v.Distinct());
        }

        public static List<PidVar> Vars(PidRLabel l)
        {
            if (l is PidVar)
                return Vars((PidVar)l);
            else if (l is PidRTuple)
                return Vars((PidRTuple)l);
            else if (l is PidRFun)
                return Vars((PidRFun)l);
            else
                Error("Invalid restricted label " + l.ToString());
            return null;
        }

        public static List<PidVar> Vars(PidVar v)
        {
            List<PidVar> l = new List<PidVar>();
            l.Add(v);
            return l;
        }

        public static List<PidVar> Vars(PidRTuple t)
        {
            List<PidVar> v = new List<PidVar>();
            for (int i = 0; i < t.Labels.Count; i++)
                v.AddRange(Vars(t.Labels[i]));
            return new List<PidVar>(v.Distinct());
        }

        public static List<PidVar> Vars(PidRFun f)
        {
            List<PidVar> v = new List<PidVar>();
            for (int i = 0; i < f.Args.Count; i++)
                v.AddRange(Vars(f.Args[i]));
            v.AddRange(Vars(f.Ret));
            return new List<PidVar>(v.Distinct());
        }

        #endregion

        #region CreateNewAlpha

        public static PidRLabel CreateNewAlpha(PidRLabel l)
        {
            if (l is PidVar)
                return CreateNewAlpha((PidVar)l);
            else if (l is PidRTuple)
                return CreateNewAlpha((PidRTuple)l);
            else if (l is PidRFun)
                return CreateNewAlpha((PidRFun)l);
            else
                Error("Invalid restricted label " + l.ToString());
            return null;
        }

        public static PidRLabel CreateNewAlpha(PidVar l)
        {
            return NewVar();
        }

        public static PidRLabel CreateNewAlpha(PidRTuple t)
        {
            List<PidRLabel> labels = new List<PidRLabel>();
            for (int i = 0; i < t.Labels.Count; i++)
                labels.Add(CreateNewAlpha(t.Labels[i]));
            return new PidRTuple(labels);
        }

        public static PidRLabel CreateNewAlpha(PidRFun f)
        {
            List<PidRLabel> args = new List<PidRLabel>();
            for (int i = 0; i < f.Args.Count; i++)
                args.Add(CreateNewAlpha(f.Args[i]));
            return new PidRFun(args, CreateNewAlpha(f.Ret));
        }

        #endregion

        #region Equate

        public static Dictionary<PidVar, PidVar> Equate(PidRLabel src, PidRLabel dest)
        {
            if ((src is PidVar) && (dest is PidVar))
                return Equate((PidVar)src, (PidVar)dest);
            else if ((src is PidRTuple) && (dest is PidRTuple))
                return Equate((PidRTuple)src, (PidRTuple)dest);
            else if ((src is PidRFun) && (dest is PidRFun))
                return Equate((PidRFun)src, (PidRFun)dest);
            Error("Unable to equate " + src.ToString() +
                " and " + dest.ToString());
            return null;
        }

        public static Dictionary<PidVar, PidVar> Equate(PidVar src, PidVar dest)
        {
            Dictionary<PidVar, PidVar> sub = new Dictionary<PidVar, PidVar>();
            sub.Add(src, dest);

            return sub;
        }

        public static Dictionary<PidVar, PidVar> Equate(PidRTuple src, PidRTuple dest)
        {
            if (src.Labels.Count != dest.Labels.Count)
                Error("Unable to equate " + src.ToString() + " and " + dest.ToString());

            Dictionary<PidVar, PidVar> sub = new Dictionary<PidVar, PidVar>();

            for (int i = 0; i < src.Labels.Count; i++)
            {
                Dictionary<PidVar, PidVar> s = Equate(src.Labels[i], dest.Labels[i]);
                foreach (PidVar v in s.Keys)
                {
                    if (sub.ContainsKey(v))
                        Error("Duplicate variable in " + src.ToString());
                    sub.Add(v, s[v]);
                }
            }

            return sub;
        }

        public static Dictionary<PidVar, PidVar> Equate(PidRFun src, PidRFun dest)
        {
            if (src.Args.Count != dest.Args.Count)
                Error("Unable to equate " + src.ToString() + " and " + dest.ToString());

            Dictionary<PidVar, PidVar> sub = new Dictionary<PidVar, PidVar>();

            for (int i = 0; i < src.Args.Count; i++)
            {
                Dictionary<PidVar, PidVar> s = Equate(src.Args[i], dest.Args[i]);
                foreach (PidVar v in s.Keys)
                {
                    if (sub.ContainsKey(v))
                        Error("Duplicate variable in " + src.ToString());
                    sub.Add(v, s[v]);
                }
            }

            Dictionary<PidVar, PidVar> ss = Equate(src.Ret, dest.Ret);
            foreach (PidVar v in ss.Keys)
            {
                if (sub.ContainsKey(v))
                    Error("Duplicate variable in " + src.ToString());
                sub.Add(v, ss[v]);
            }

            return sub;
        }

        #endregion

        #region Sub

        public static PidLabel Sub(Dictionary<PidVar, PidBase> sub, PidLabel label, bool join)
        {
            if (label is PidBase)
                return Sub(sub, (PidBase)label, join);
            else if (label is PidTuple)
                return Sub(sub, (PidTuple)label, join);
            else if (label is PidFun)
                return Sub(sub, (PidFun)label, join);
            else
                Error("Invalid process label " + label.ToString());
            return null;
        }

        public static PidBase Sub(Dictionary<PidVar, PidBase> sub, PidBase label, bool join)
        {
            if (label.Pidvs == null || label.Pidvs.Count == 0)
                return label;

            List<List<PidExpr>> pids = new List<List<PidExpr>>();
            List<List<PidVar>> vars = new List<List<PidVar>>();

            pids.Add(label.Pids);
            foreach (PidVar v in label.Pidvs)
            {
                if (sub.ContainsKey(v))
                {
                    pids.Add(sub[v].Pids);
                    vars.Add(sub[v].Pidvs);
                }
                else
                {
                    List<PidVar> l = new List<PidVar>();
                    l.Add(v);
                    vars.Add(l);
                }
            }

            pids.RemoveAll(item => item == null);
            vars.RemoveAll(item => item == null);

            IEnumerable<PidExpr> newPids = null;
            IEnumerable<PidVar> newVars = null;
            if (pids.Count > 0)
            {
                newPids = pids[0];
                if (join)
                {
                    for (int i = 1; i < pids.Count; i++)
                        newPids = newPids.Union(pids[i]);
                }
                else
                {
                    for (int i = 1; i < pids.Count; i++)
                        newPids = newPids.Intersect(pids[i]);
                }
            }
            if (vars.Count > 0)
            {
                newVars = vars[0];
                for (int i = 1; i < vars.Count; i++)
                    newVars = newVars.Union(vars[i]);
            }

            List<PidVar> pv = (newVars == null) ? null : new List<PidVar>(newVars);
            List<PidExpr> pe = (newPids == null) ? null : new List<PidExpr>(newPids);

            return new PidBase(pv, pe);
        }

        public static PidTuple Sub(Dictionary<PidVar, PidBase> sub, PidTuple label, bool join)
        {
            List<PidLabel> labels = new List<PidLabel>();
            for (int i = 0; i < label.Labels.Count; i++)
                labels.Add(Sub(sub, label.Labels[i], join));
            return new PidTuple(labels);
        }

        public static PidFun Sub(Dictionary<PidVar, PidBase> sub, PidFun label, bool join)
        {
            bool alphaConvert = false;

            List<PidVar> subVars = new List<PidVar>();
            foreach (PidVar v in sub.Keys)
            {
                subVars.Add(v);
                subVars.AddRange(sub[v].Pidvs);
            }

            foreach (PidRLabel a in label.Args)
            {
                if (Vars(a).Intersect(subVars).Count() > 0)
                    alphaConvert = true;
            }

            PidFun res = label;

            if (alphaConvert)
            {
                List<PidRLabel> newArgs = new List<PidRLabel>();
                foreach (PidRLabel a in label.Args)
                    newArgs.Add(CreateNewAlpha(a));
                // Create a pid tuple for ease of calculating the substitution
                PidRTuple src = new PidRTuple(label.Args);
                PidRTuple dest = new PidRTuple(newArgs);
                Dictionary<PidVar, PidVar> asub = Equate(src, dest);
                res = AlphaConvert(label, asub, join);
            }

            // Now return the final function
            List<PidRLabel> resArgs = res.Args;
            PidLabel resRet = Sub(sub, res.Ret, join);
            return new PidFun(resArgs, resRet);
        }

        #endregion

        #region Alpha

        public static PidRLabel Alpha(Dictionary<PidVar, PidVar> sub, PidRLabel label)
        {
            if (label is PidVar)
                return Alpha(sub, (PidVar)label);
            else if (label is PidRTuple)
                return Alpha(sub, (PidRTuple)label);
            else if (label is PidRFun)
                return Alpha(sub, (PidRFun)label);
            else
                Error("Invalid restricted label " + label.ToString());
            return null;
        }

        public static PidRLabel Alpha(Dictionary<PidVar, PidVar> sub, PidVar label)
        {
            if (sub.ContainsKey(label))
                return sub[label];
            else
                return label;
        }

        public static PidRLabel Alpha(Dictionary<PidVar, PidVar> sub, PidRTuple label)
        {
            List<PidRLabel> labels = new List<PidRLabel>();
            for (int i = 0; i < label.Labels.Count; i++)
                labels.Add(Alpha(sub, label.Labels[i]));
            return new PidRTuple(labels);
        }

        public static PidRLabel Alpha(Dictionary<PidVar, PidVar> sub, PidRFun label)
        {
            List<PidRLabel> args = new List<PidRLabel>();
            for (int i = 0; i < label.Args.Count; i++)
                args.Add(Alpha(sub, label.Args[i]));
            return new PidRFun(args, Alpha(sub, label.Ret));
        }

        #endregion

        #region CreateFromType

        public static PidRLabel CreateFromType(Type t)
        {
            if (t is SimpleType)
                return CreateFromType((SimpleType)t);
            else if (t is AtomType)
                return CreateFromType((AtomType)t);
            else if (t is ListType)
                return CreateFromType((ListType)t);
            else if (t is TupleType)
                return CreateFromType((TupleType)t);
            else if (t is FunType)
                return CreateFromType((FunType)t);
            else
                Error("Invalid type");
            return null;
        }

        public static PidVar CreateFromType(SimpleType t)
        {
            return NewVar();
        }

        public static PidVar CreateFromType(AtomType t)
        {
            return NewVar();
        }

        public static PidRLabel CreateFromType(ListType t)
        {
            return CreateFromType(t.ElementType);
        }

        public static PidRTuple CreateFromType(TupleType t)
        {
            List<PidRLabel> labels = new List<PidRLabel>();
            for (int i = 0; i < t.Types.Count; i++)
                labels.Add(CreateFromType(t.Types[i]));
            return new PidRTuple(labels);
        }

        public static PidRFun CreateFromType(FunType t)
        {
            List<PidRLabel> args = new List<PidRLabel>();
            for (int i = 0; i < t.Args.Count; i++)
                args.Add(CreateFromType(t.Args[i]));
            return new PidRFun(args, CreateFromType(t.Ret));
        }

        #endregion

        #region FromRestricted

        public static PidLabel FromRestricted(PidRLabel src)
        {
            if (src is PidVar)
                return FromRestricted((PidVar)src);
            else if (src is PidRTuple)
                return FromRestricted((PidRTuple)src);
            else if (src is PidRFun)
                return FromRestricted((PidRFun)src);
            else
                Error("Invalid restricted process label");
            return null;
        }             
                      
        public static PidLabel FromRestricted(PidVar src)
        {
            return new PidBase(new List<PidVar>() { src }, null); 
        }             
                      
        public static PidLabel FromRestricted(PidRTuple src)
        {
            List<PidLabel> labels = new List<PidLabel>();
            for (int i = 0; i < src.Labels.Count; i++)
                labels.Add(FromRestricted(src.Labels[i]));
            return new PidTuple(labels);
        }

        public static PidLabel FromRestricted(PidRFun src)
        {
            return new PidFun(src.Args, FromRestricted(src.Ret));
        }

        #endregion

        #region Unify

        public static Dictionary<PidVar, PidBase> Unify(PidRLabel src, PidLabel dest)
        {
            if (src is PidVar)
                if (dest is PidVar)
                    return Unify((PidVar)src, (PidVar)dest);
                else if (dest is PidBase)
                    return Unify((PidVar)src, (PidBase)dest);
                else
                    Error("Unable to unify " + src.ToString() + " and " + dest.ToString());
            else if ((src is PidRTuple) && (dest is PidTuple))
                return Unify((PidRTuple)src, (PidTuple)dest);
            else if ((src is PidRFun) && (dest is PidFun))
                return Unify((PidRFun)src, (PidFun)dest);
            else
                Error("Unable to unify " + src.ToString() + " and " + dest.ToString());
            return null;
        }

        public static Dictionary<PidVar, PidBase> Unify(PidVar src, PidVar dest)
        {
            Dictionary<PidVar, PidBase> dict = new Dictionary<PidVar, PidBase>();
            dict.Add(src, new PidBase(new List<PidVar>() { dest }, null));
            return dict;
        }

        public static Dictionary<PidVar, PidBase> Unify(PidVar src, PidBase dest)
        {
            Dictionary<PidVar, PidBase> dict = new Dictionary<PidVar, PidBase>();
            dict.Add(src, dest);
            return dict;
        }

        public static Dictionary<PidVar, PidBase> Unify(PidRTuple src, PidTuple dest)
        {
            if (src.Labels.Count != dest.Labels.Count)
                Error("Unable to unify " + src.ToString() + " and " + dest.ToString());

            Dictionary<PidVar, PidBase> dict = new Dictionary<PidVar, PidBase>();

            for (int i = 0; i < src.Labels.Count; i++)
            {
                Dictionary<PidVar, PidBase> sub = Unify(src.Labels[i], dest.Labels[i]);
                foreach (PidVar v in sub.Keys)
                {
                    if (dict.ContainsKey(v))
                        Error("Duplicate variable in " + src.ToString());
                    dict.Add(v, sub[v]);
                }
            }

            return dict;
        }

        public static Dictionary<PidVar, PidBase> Unify(PidRFun src, PidFun dest)
        {
            if (src.Args.Count != dest.Args.Count)
                Error("Unable to unify " + src.ToString() + " and " + dest.ToString());

            Dictionary<PidVar, PidBase> dict = new Dictionary<PidVar, PidBase>();

            for (int i = 0; i < src.Args.Count; i++)
            {
                Dictionary<PidVar, PidBase> sub = Unify(src.Args[i], dest.Args[i]);
                foreach (PidVar v in sub.Keys)
                {
                    if (dict.ContainsKey(v))
                        Error("Duplicate variable in " + src.ToString());
                    dict.Add(v, sub[v]);
                }
            }

            Dictionary<PidVar, PidBase> ssub = Unify(src.Ret, dest.Ret);
            foreach (PidVar v in ssub.Keys)
            {
                if (dict.ContainsKey(v))
                    Error("Duplicate variable in " + src.ToString());
                dict.Add(v, ssub[v]);
            }

            return dict;
        }

        #endregion
    }
}
